/*
 * Alloy Analyzer 4 -- Copyright (c) 2006-2008, Felix Chang
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */

package edu.ut.ece382c.valloy.parser;

import java.io.BufferedReader;
import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.IOException;
import java.io.Writer;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Map;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Stack;
import java.util.Vector;
import java.util.Map.Entry;

import edu.mit.csail.sdg.alloy4.ConstList;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorFatal;
import edu.mit.csail.sdg.alloy4.ErrorSyntax;
import edu.mit.csail.sdg.alloy4.ErrorType;
import edu.mit.csail.sdg.alloy4.Pair;
import edu.mit.csail.sdg.alloy4.Pos;
import edu.mit.csail.sdg.alloy4.SafeList;
import edu.mit.csail.sdg.alloy4.Version;
import edu.mit.csail.sdg.alloy4.ConstList.TempList;
//import edu.mit.csail.sdg.alloy4compiler.ast.ExprQuant;


import edu.ut.ece382c.valloy.ast.ExprBadJoin;
import edu.ut.ece382c.valloy.ast.ExprBinary;
import edu.ut.ece382c.valloy.ast.ExprITE;
import edu.ut.ece382c.valloy.ast.ExprList;
import edu.ut.ece382c.valloy.ast.Node;
import edu.ut.ece382c.valloy.ast.Command;
import edu.ut.ece382c.valloy.ast.CommandScope;
import edu.ut.ece382c.valloy.ast.Expr;
import edu.ut.ece382c.valloy.ast.ExprUnary;
import edu.ut.ece382c.valloy.ast.ExprVar;
import edu.ut.ece382c.valloy.ast.ExprConstant;
import edu.ut.ece382c.valloy.ast.Func;
import edu.ut.ece382c.valloy.ast.Sig;
import edu.ut.ece382c.valloy.ast.ExprList.Op;
import static edu.ut.ece382c.valloy.ast.Type.EMPTY;


/** Mutable; this class represents an Alloy module; equals() uses object identity. */

final class Module extends Node {

    /** {@inheritDoc} */
    @Override public final Pos pos() { return modulePos; }

    /** {@inheritDoc} */
    @Override public final Pos span() { return modulePos; }

    //============================================================================================================================//

    /** Mutable; this class represents an untypechecked Alloy module import statement; equals() uses object identity. */
    public static final class Open {
        /** The position in the original model where this "open" statement was declared; never null. */
        public final Pos pos;
        /** The alias for this open declaration; always a nonempty string. */
        public final String alias;
        /** The unmodifiable list of instantiating arguments. */
        public final ConstList<String> args;
        /** The relative filename for the file being imported, without the final ".als" part; always a nonempty string. */
        public final String filename;
        /** Whether this is a private open or not. */
        final boolean isPrivate;
        
        /** Constructs an Open object. */
        private Open(Pos pos, boolean isPrivate, String alias, ConstList<String> args, String filename) {
            this.pos=pos; 
            this.isPrivate=isPrivate; 
            this.alias=alias; 
            this.args=args; 
            this.filename=filename;
        }

        
        @Override public final String toString()  { 
        	StringBuilder sb=new StringBuilder(); 
        	toString(sb, 0); 
        	return sb.toString(); 
        }

        /** {@inheritDoc} */
        public final void toString(StringBuilder out, int indent) {
        	
        	for(int i=0; i<indent; i++) { 
        		out.append(' '); 
        	}
        	
        	if (isPrivate)
        		out.append("private ");
        	
        	out.append("open " + filename);
        	
        	if (args != null && args.size() != 0) {
        		out.append("[");
        		String argList = "";
        		for(String a: args){
        			if(argList != "") argList += ", ";
        			argList += a;
        		}
        			
        		out.append(argList + "]");
        	}
        	
        	if (alias != null && alias != "") {
        		out.append(" as " + alias);
        	}
        	
        }
    }

    //============================================================================================================================//

    //============================================================================================================================//

    /** The world that this Module belongs to. */
    private final Module world;

    /** The simplest path pointing to this Module; it is always equal to this.paths.get(0) */
    @SuppressWarnings("unused") private final String path;

    /** The list of paths pointing to this Module; it is always nonempty and already sorted by Util.slashComparator */
    private final List<String> paths;

    /**
     * 1: has seen the "module" line
     * 2: has seen the "open" lines
     * 3: has seen the "sig/pred/fun/fact/assert/check/run" commands
     */
    private int status = 0;

    /** The position of the "MODULE" line at the top of the file; Pos.UNKNOWN if the line has not been parsed from the file yet. */
    private Pos modulePos = Pos.UNKNOWN;

    /** The text of the "MODULE" line at the top of the file; "unknown" if the line has not be parsed from the file yet. */
    private String moduleName = "unknown";

    /** Each param is mapped to its corresponding SigAST (or null if we have not resolved it). */
    private List<ExprVar> moduleParams = new ArrayList<ExprVar>();
    
    /** Each alias is mapped to its corresponding "open" statement. */
    private final Map<String,Open> opens = new LinkedHashMap<String,Open>();

    /** Each sig name is mapped to its corresponding SigAST. */
    private final Map<String,Sig> sigs = new LinkedHashMap<String,Sig>();

    /** The current name resolution mode (0=pure) (1=Alloy 4.1.3 and older) (2=new) */
    int resolution = 1;

    /** Each func name is mapped to a nonempty list of ast.Func objects. */
    private final Map<String,SafeList<Func>> functions = new LinkedHashMap<String,SafeList<Func>>();
    
    private final Map<String,SafeList<Func>> resolvedFunctions = new LinkedHashMap<String,SafeList<Func>>();
    
    /** Each macro name is mapped to a MacroAST object. */
    private final Map<String,Macro> macros = new LinkedHashMap<String,Macro>();

    /** Each assertion name is mapped to either an untypechecked Exp, or a typechecked ExprVar with its value==the assertion. */
    private final Map<String,Expr> asserts = new LinkedHashMap<String,Expr>();

    /** The list of facts; each fact is either an untypechecked Exp or a typechecked Expr. */
    private final List<Pair<String,Expr>> facts = new ArrayList<Pair<String,Expr>>();

    /** The list of (CommandName,Command,Expr) triples; NOTE: duplicate command names are allowed. */
    private final List<Command> commands = new ArrayList<Command>();

    /** The VAlloy class hierarchy for this module */
    private ModelClassHierarchy classHierarchy;
    
    /** To hold all of the hierarchies within the model*/
    private Vector<ModelClassHierarchy> modelHierarchies;
    
    /** The temporary VAlloy class map */
    private TempClassMap classMap;
    
    /** Does the model hold VAlloy classes?*/
    private boolean VAlloy;
    
    /** Does the model hold VAlloy classes?*/
    private final String valloyRootObjectName = "DUMMY_VALLOY_ROOT_OBJECT";
    
    /**
     * Constructs a new Module object
     * @param world - the world that this Module belongs to (null if this is the beginning of a new World)
     * @param filename - the filename corresponding to this module
     * @param path - one of the path pointing to this module
     */
    public Module(Module world, String filename, String path) throws Err {
        if (world==null) { if (path.length()>0) throw new ErrorFatal("Root module misparsed by parser."); else world=this; }
        this.world=world;
        this.path=path;
        this.paths=new ArrayList<String>(1);
        this.paths.add(path);
        this.classHierarchy = new  ModelClassHierarchy(valloyRootObjectName);
        this.modelHierarchies = new  Vector<ModelClassHierarchy>();
        this.classMap = new TempClassMap (this);
        this.VAlloy = false;
        if (filename!=null && filename.length()>0) this.modulePos=new Pos(filename,1,1);
    }

    //============================================================================================================================//

    /** Generate an error message saying the given keyword is no longer supported. */
    static ErrorSyntax hint (Pos pos, String name) {
        String msg="The name \""+name+"\" cannot be found.";
        if ("exh".equals(name) || "exhaustive".equals(name) || "part".equals(name) || "partition".equals(name))
            msg=msg+" If you are migrating from Alloy 3, please see Help->QuickGuide on how to translate models that use the \""
            +name+"\" keyword.";
        return new ErrorSyntax(pos, msg);
    }
    
    /** Throw an exception if the name is already used, or has @ or /, or is univ/Int/none. */
    private void dup(Pos pos, String name, boolean checkSig) throws Err {
        if (name.length()==0)     throw new ErrorSyntax(pos, "Name cannot be empty");
        if (name.indexOf('@')>=0) throw new ErrorSyntax(pos, "Name cannot contain the \'@\' character");
        if (name.indexOf('/')>=0) throw new ErrorSyntax(pos, "Name cannot contain the \'/\' character");
        if (name.equals("univ"))  throw new ErrorSyntax(pos, "\'univ\' is a reserved keyword.");
        if (name.equals("Int"))   throw new ErrorSyntax(pos, "\'Int\' is a reserved keyword.");
        if (name.equals("none"))  throw new ErrorSyntax(pos, "\'none\' is a reserved keyword.");
        if (checkSig && sigs.containsKey(name))
            throw new ErrorSyntax(pos, "\""+name+"\" is already the name of a sig/parameter in this module.");
    }
    
    
    /** Returns a short description for this module. */
    @Override public String toString() {
    	
    	String out = "";
    	
        out += "module " + moduleName;
        
        if (moduleParams != null && moduleParams.size() != 0) {
        	String paramlist = "";
        	boolean exact = false;
        	for(ExprVar e: moduleParams) {
        		if (paramlist.length() != 0) paramlist += ", ";
        		if (e == null) {
        			//
        			// The parser encodes 'exactly' by including
        			// a null expression before the parameter name
        			//
        			exact = true;
        		} else {
        			// check if this is an 'exactly' parameter
        			if (exact) paramlist += "exactly ";
        			exact = false;
        			
        			// add parameter name to the list
        			paramlist += e.toString();
        		}
        	}	
        	out += "[" + paramlist + "]";
        }
        return out;
    }

    //============================================================================================================================//

    /** Returns a pointer to the root module in this world. */
    public Module getRootModule() { return world; }

    /** Returns the text of the "MODULE" line at the top of the file; "unknown" if the line has not be parsed from the file yet. */
    public String getModelName() { return moduleName; }

    /** Returns an unmodifiable copy of the current list of OPEN statements. */
    public ConstList<Open> getOpens() {
        TempList<Open> ans = new TempList<Open>(opens.size());
        for(Map.Entry<String,Open> e: opens.entrySet()) ans.add(e.getValue());
        return ans.makeConst();
    }

    /** Add the "MODULE" declaration. */
    void addModelName(Pos pos, String moduleName, List<ExprVar> list) throws Err {
        this.moduleName=moduleName;
        this.modulePos=pos;
        this.moduleParams = list;
        this.status=1; 
    }

    /** Add util/sequniv to the list of declarations. */
    void addSeq(Pos pos) throws Err {
        int oldStatus=status;
        status=0;
        try {
            addOpen(pos, null, ExprVar.make(pos, "util/sequniv"), null, ExprVar.make(pos, "seq"));
        } finally {
            status=oldStatus;
        }
    }

    /** Add an OPEN declaration. */
    void addOpen(Pos pos, Pos isPrivate, ExprVar name, List<ExprVar> args, ExprVar alias) throws Err {
    	
        if (status>2) throw new ErrorSyntax(pos,
           "The \"open\" declaration must occur before any\n" + "sig/pred/fun/fact/assert/check/run command.");
        status=2;
        
        String as = (alias==null ? "" : alias.label);
        final TempList<String> newlist = new TempList<String>(args==null ? 0 : args.size());
        if (args!=null) for(int i=0; i<args.size(); i++) {
            ExprVar arg=args.get(i);
            if (arg.label.length()==0)      throw new ErrorSyntax(arg.span(), "Argument cannot be empty.");
            if (arg.label.indexOf('@')>=0)  throw new ErrorSyntax(arg.span(), "Argument cannot contain the \'@\' chracter.");
            newlist.add(arg.label);
        }
        
        Open x = new Open(pos, isPrivate!=null, as, newlist.makeConst(), name.label);
        opens.put(as,x);
    }
    //============================================================================================================================//

    

    /** Builds the VAlloy class hierarchy, support sigs, and facts */
	public boolean resolveClasses () throws Err {
		/**Temporary place to hold the classes as we add them to the tree*/
		Stack<String> toAdd = new Stack<String>(); 
		String currentClass = null;
		String parentName = null;
		
		//case where there aren't really any classes in this model
		if (classMap.returnAll().size()<=1)
			return true;
		
		//Create one hierarchy tree using Object as the root
		for (String vClassName: classMap.returnAll()) {
			toAdd.clear();
			toAdd.push(vClassName);
			while (!toAdd.empty()){
				currentClass = toAdd.pop();
				parentName = classMap.get(currentClass).getParent().getName();
				if (classMap.contains(parentName) || parentName == valloyRootObjectName){
					if (classHierarchy.contains(parentName)){
						classHierarchy.add(currentClass, parentName);	
					}
					else {
						if (toAdd.contains(parentName)){
							throw new ErrorType(classMap.get(currentClass).getPosition(), "Cycle in class hierarcy detected:\n" 
													+ parentName + " --> " + currentClass);
						}
						toAdd.push(currentClass);
						toAdd.push(parentName);
					}
						
				}
				else {
					//the specified parent is not in our map, could be in a dependency
					if (opens.isEmpty()){
						//if there are no dependencies, throw error: undefined parent 
						throw new ErrorType(classMap.get(currentClass).getPosition(), "Undefined parent class:\n" 
											+ classMap.get(currentClass).getParent().getName() + " referenced by " + currentClass);
					}
					else{
						//TODO: finish Multimodule VAlloy case
						for (String key: opens.keySet()){
							Module parentModule = new Module (this.world, opens.get(key).filename, this.path);
							parentModule.parse();
						}
					}
				}
			}
		}

		//Add the ValloyClass signature that all Valloy Class Names will extend
		//TODO: make these names come from a common place: VExt, VAlloyClassName_
		// valloyClassNameSuffix, valloyClassRelation 
		ExprVar valloyExtend = ExprVar.make(Pos.UNKNOWN, "VExt");
		ExprVar valloyClassNameExpr = ExprVar.make(Pos.UNKNOWN,"VAlloyRootClass");
		final String valloyClassNameSuffix = "_VAlloyClassName"; 
		final String valloyClassRelation = "class";
		
		Vector<ExprVar> valloyExtendList = new Vector<ExprVar>();
		valloyExtendList.add(valloyExtend);
		Vector <Decl> declarations = new Vector<Decl>();
		Decl relation = new Decl(null, null, null, valloyExtendList,
								ExprUnary.Op.LONE.make(Pos.UNKNOWN, valloyClassNameExpr));
		declarations.add(relation);
		addSig(null, Pos.UNKNOWN, valloyClassNameExpr.toString(), Pos.UNKNOWN,
				null ,null , null, null, null, null, declarations, Pos.UNKNOWN, null);
		
		//We now remove the root class and use each child as a root for an independent hierarchy
		modelHierarchies=classHierarchy.split(valloyRootObjectName);
		
		
		//and for each independent hierarchy, create the appropriate facts
		for (ModelClassHierarchy indepHierarchy: modelHierarchies){		
			//Create fact that defines the Class hierarchy 
			//first we create a lost of expressions that will make up the body:
			Vector<Expr> body = new Vector<Expr>(); 

			
			//add relationship of root class with ValloyClassName
			Vector<ExprVar> relList = new Vector<ExprVar>();
			relList.add(ExprVar.make(Pos.UNKNOWN, valloyClassRelation));
			Vector<Decl> declList = new Vector<Decl>();						
			declList.add(new Decl(null, null, null,relList,ExprUnary.Op.ONE.make(Pos.UNKNOWN, valloyClassNameExpr)));
			sigs.get(indepHierarchy.getRoot().getName()).addFileds(declList);
			
			// add then the special clause for the root Class fact
			Expr extExpr = ExprVar.make(Pos.UNKNOWN, "VExt");
			Expr rootExt = ExprBadJoin.make(Pos.UNKNOWN, Pos.UNKNOWN, ExprVar.make(Pos.UNKNOWN, indepHierarchy.getRoot().getName() + valloyClassNameSuffix), extExpr);
			Expr rootExpr = ExprUnary.Op.NO.make(Pos.UNKNOWN, rootExt);
			body.add(rootExpr);
			
			// traverse the tree to create a hierarchy
			Stack<ValloyClass> treeNodes = new Stack<ValloyClass>();
			treeNodes.addAll(indepHierarchy.getRoot().getChildren());
			while (!treeNodes.empty()){
				ValloyClass child = treeNodes.pop();
				Expr classExt = ExprBadJoin.make(Pos.UNKNOWN, Pos.UNKNOWN, ExprVar.make(Pos.UNKNOWN, child.getName() + valloyClassNameSuffix), extExpr);
				body.add(ExprBinary.Op.EQUALS.make(Pos.UNKNOWN, Pos.UNKNOWN, classExt,ExprVar.make(Pos.UNKNOWN, child.getParent().getName() + valloyClassNameSuffix)));
				treeNodes.addAll(child.getChildren());
			}
			
			// create the hierarchy fact
			this.addFact(Pos.UNKNOWN, indepHierarchy.getRoot().getName() + "_VAlloyHierarchy", ExprList.make(Pos.UNKNOWN, Pos.UNKNOWN, Op.AND,body));		
			
			
			// create sigs for each Valloy class name
			Vector<ExprVar> listOfValloyClassNameExpr = new Vector<ExprVar>();
			listOfValloyClassNameExpr.add(valloyClassNameExpr);
			for (ValloyClass vClass : indepHierarchy.getAll()){
				//TODO: is there a better way to create the Expr "Extends", see below
				Sig sg = addSig(null, Pos.UNKNOWN, vClass.getName() + valloyClassNameSuffix,
						null, null , Pos.UNKNOWN, null, null, ExprVar.make(Pos.UNKNOWN,"extends"),
						listOfValloyClassNameExpr, null, Pos.UNKNOWN, null);
				sigs.put(vClass.getName() + "_VAlloyClassName", sg);
			}
			
			/* Now add this fact that breaks all objects belonging to the hierarchy into the respective classes
			from the dimension example:
			fact ObjectClasses {
		        ((Object - Dimension).class = Object_Class
		        or Object - Dimension = none)
		    and
		        ((Dimension - Dimension3D).class = Dimension_Class
		        or Dimension - Dimension3D = none)
		    and
		        (Dimension3D.class = Dimension3D_Class
		        or Dimension3D = none)
			}*/
			treeNodes.clear();
			body.clear();
			treeNodes.push(indepHierarchy.getRoot());
			while (!treeNodes.empty()){
				ValloyClass node = treeNodes.pop();
				Vector<Expr> childSets = new Vector<Expr>();
				for (ValloyClass child: node.getChildren()){	
					childSets.add(ExprVar.make(Pos.UNKNOWN,child.getName()));
				}
				Expr subtracted= null;
				Expr lhs,lhsNull = null;
				//If the class has children, then only objects not belonging to the children have the run-time type of this class
				if  (childSets.size()>=1){
					subtracted = childSets.remove(0);
					for ( Expr next : childSets){
						subtracted = ExprBinary.Op.PLUS.make(Pos.UNKNOWN, Pos.UNKNOWN, subtracted, next);
					}
					//add parens
					subtracted =  ExprUnary.Op.NOOP.make(Pos.UNKNOWN, subtracted);
					//parent objects minus children objects
					lhs = ExprBinary.Op.MINUS.make(Pos.UNKNOWN, Pos.UNKNOWN, ExprVar.make(Pos.UNKNOWN, node.getName()),
							subtracted);
					//add parens
					lhs = ExprUnary.Op.NOOP.make(Pos.UNKNOWN, lhs);
				}
				else {
					lhs = ExprVar.make(Pos.UNKNOWN, node.getName());	
				}
				lhsNull = lhs;// reuse lhs value for second part of clause
				
				//add the class relation to the set
				lhs = lhs.join(ExprVar.make(Pos.UNKNOWN, valloyClassRelation));
				Expr clause = ExprBinary.Op.EQUALS.make(Pos.UNKNOWN, Pos.UNKNOWN, 
									lhs,
									ExprVar.make(Pos.UNKNOWN, node.getName() + valloyClassNameSuffix));
				
				//add second part of clause, in case lhs is an empty set: Object - Children = none
				lhsNull = lhsNull.equal(ExprConstant.EMPTYNESS);
				
				//OR the two parts
				clause = clause.or(lhsNull);
				
				body.add(clause);
				treeNodes.addAll(node.getChildren());
			}
			this.addFact(Pos.UNKNOWN, indepHierarchy.getRoot().getName() +"_ValloyClassBreakdown",
						ExprList.make(Pos.UNKNOWN, Pos.UNKNOWN, Op.AND, body));					
		
			//Add getClass() function for this hierarchy
			/*fun Object::getClass[ ]: ValloyClassName {
			    this.ValloyClass
			}*/
			
			//Vector<Decl> returnTypeList = new Vector<Decl>();
			//Decl returnType = new Decl(null, null, null, null,
			//						ExprUnary.Op.LONE.make(Pos.UNKNOWN, valloyClassNameExpr));
			//returnTypeList.add(returnType);
			addFunc(null, null,null ,"getClass",
					ExprVar.make(Pos.UNKNOWN, indepHierarchy.getRoot().getName()),
					null,valloyClassNameExpr, ExprVar.make(Pos.UNKNOWN, "this").join(ExprVar.make(Pos.UNKNOWN, valloyClassRelation)));		
		
		}	
		
		//System.out.print(classHierarchy.toString());
		return true;
	}
    
    /** Failed attempt to have modules parse themselves*/
	private Module parse (){
		try{
			CompLexer lexer = new CompLexer(new BufferedReader(new FileReader(this.path)));
			lexer.alloy_module = this;
			
			// Create parser.  Lexer is wrapped in a CompFilter object to deal
			// with some syntax ambiguities that the parser cannot handle
			CompParser parser = new CompParser(new CompFilter(lexer));
			parser.alloymodule = lexer.alloy_module;
			
			// Parse!
			parser.parse();
			return this;
		}
		catch (FileNotFoundException fnf){
			//TODO: Throw this up or handle here?
			System.out.println ("File Not Found Exception while parsing module"+
					this.path + "\n" +
					fnf.getMessage());
		}
		catch (Exception exc){
			//TODO: something else went wrong
			System.out.println ("Unknown Exception while parsing module:\n"+
								this.path + "\n" +
								exc.getMessage());
		}
		return null;
	}
	
	
    /** Add a class declaration. */
    Sig addClass(List<ExprVar> hints, Pos pos, String name, Pos isAbstract, Pos isLone, Pos isOne, Pos isSome, Pos isPrivate,
        ExprVar par, List<ExprVar> parents, List<Decl> fields, Pos endOfFields, Expr fact) throws Err {
        pos = pos.merge(isAbstract).merge(isLone).merge(isOne).merge(isSome);
        status=3;
        dup(pos, name, true);
        
        Pos subset=null, subsig=null;
        
        if (par!=null) {
            if (par.label.equals("extends")) { 
            	subsig=par.span().merge(parents.get(0).span()); 
            	if (!classMap.add(name, parents.get(0).toString()) == true){
            		throw new ErrorFatal(pos, "Could not add class \"" + name + "\" to internal class map");
            	}
            	else {
            		classMap.get(name).setPosition(pos);
            	}
            } else { 
            	//
            	// No 'subset' inheritance allowed.  Don't really know what that means...
            	//
            	// subset=par.span(); 
            	// for(ExprVar p:parents) 
            	//	subset=p.span().merge(subset);
            	//
            	throw new ErrorSyntax(pos, "Only 'extends' is allowed");
            }
        }
        
    	//
    	// if top-level class, add Object as a parent signature
    	//
        if (subsig == null && opens.isEmpty())
        {
        	assert(parents == null);
        	
        	//subsig = Pos.UNKNOWN;
        	//parents = new ArrayList<ExprVar>(1); 
        	//parents.add(ExprVar.make(null, valloyRootObjectName));
        	if (classMap.add(name, valloyRootObjectName) == false){
        		throw new ErrorSyntax(pos, valloyRootObjectName + " class name is reseved.");
        	}
        	else {
        		classMap.get(name).setPosition(pos);
        	}
        }
        if (subsig == null && !opens.isEmpty()){
        	//TODO: Handle case where other modules are referenced?
    		throw new ErrorFatal(pos, "Multimodule VAlloy not implemented.");
        }
        
        //
        // TODO classes support facts?
        //
        // Special case for empty appended facts.  The parser will pass a constant TRUE
        // if the fact body is empty.  Use null to indicate an empty fact
        //
        if (fact instanceof ExprConstant) {
        	ExprConstant c = (ExprConstant)fact;
        	if (c.op == ExprConstant.Op.TRUE) {
        		fact = null;
        	}
        }
        
        assert(parents != null);
        assert(parents.size() == 1);
     
        //
        // Translate class to signature 
        //
        Sig sg = new Sig(pos, EMPTY, name, isAbstract, isLone, isOne, isSome, subsig, subset, isPrivate, parents, fields, fact);
        sigs.put(name, sg);
        return sg;
    }
    
    
    //============================================================================================================================//

    /** Add a sig declaration. */
    Sig addSig(List<ExprVar> hints, Pos pos, String name, Pos isAbstract, Pos isLone, Pos isOne, Pos isSome, Pos isPrivate,
        ExprVar par, List<ExprVar> parents, List<Decl> fields, Pos endOfFields, Expr fact) throws Err {
        pos = pos.merge(isAbstract).merge(isLone).merge(isOne).merge(isSome);
        status=3;
        dup(pos, name, true);
        
        Pos subset=null, subsig=null;
        
        if (par!=null) {
            if (par.label.equals("extends")) { 
            	subsig=par.span().merge(parents.get(0).span()); 
            } else { 
            	subset=par.span(); 
            	for(ExprVar p:parents) 
            		subset=p.span().merge(subset); 
            }
        }
        
        //
        // Special case for empty appended facts.  The parser will pass a constant TRUE
        // if the fact body is empty.  Use null to indicate an empty fact
        //
        if (fact instanceof ExprConstant) {
        	ExprConstant c = (ExprConstant)fact;
        	if (c.op == ExprConstant.Op.TRUE) {
        		fact = null;
        	}
        }
        
        Sig sg = new Sig(pos, EMPTY, name, isAbstract, isLone, isOne, isSome, subsig, subset, isPrivate, parents, fields, fact);
        sigs.put(name, sg);
        return sg;
    }

    /** The list of ENUMS in this module. */
    private final List<Pair<Sig,Integer>> enums = new ArrayList<Pair<Sig,Integer>>();

    /** Add an enumeration. */
    void addEnum(Pos pos, Pos priv, ExprVar name, List<ExprVar> parents, List<ExprVar> atoms, Pos closingBracket) throws Err {
    	//
    	// TODO VALLOY what are enums? maybe treat differently to print them correctly.
    	//
        ExprVar LEAF = ExprVar.make(null,"leaf");
        ExprVar EXTENDS = ExprVar.make(null, "extends");
        ExprVar THIS = ExprVar.make(null, "this/"+name);
        List<ExprVar> THESE = Arrays.asList(THIS);
        if (atoms==null || atoms.size()==0) throw new ErrorSyntax(pos, "Enumeration must contain at least one name.");
        if (parents!=null) parents = new ArrayList<ExprVar>(parents);
        ExprVar inOrExtend = (parents!=null && parents.size()>0) ? parents.remove(parents.size()-1) : null;
        if (inOrExtend!=null && inOrExtend.label.charAt(0)=='i') throw new ErrorSyntax(pos, "Enumeration signatures cannot derive from a subset signature.");
        Sig ans = addSig(Arrays.asList(LEAF), name.pos, name.label, name.pos, null, null, null, priv, inOrExtend, parents, null, null, null);
        enums.add(new Pair<Sig,Integer>(ans, atoms.size()));
        for(ExprVar a:atoms) addSig(null, a.pos, a.label, null, null, a.pos, null, priv, EXTENDS, THESE, null, null, null);
    }
    
    /** Returns an unmodifiable list of all signatures defined inside this module. */
    public SafeList<Sig> getAllSigs() {
        SafeList<Sig> x = new SafeList<Sig>(sigs.size());
        for(Map.Entry<String,Sig> e:sigs.entrySet()) x.add(e.getValue());
        return x.dup();
    }

    //============================================================================================================================//

    /** Add a MACRO declaration. */
    void addMacro(Pos p, Pos isPrivate, String n, List<ExprVar> decls, Expr v) throws Err {
        if (!Version.experimental) throw new ErrorSyntax(p, "LET declaration is allowed only inside a toplevel paragraph.");
        ConstList<ExprVar> ds = ConstList.make(decls);
        status=3;
        dup(p, n, false);
        for(int i=0; i<ds.size(); i++) for(int j=i+1; j<ds.size(); j++)
          if (ds.get(i).label.equals(ds.get(j).label))
             throw new ErrorSyntax(ds.get(j).span(), "The parameter name \""+ds.get(j).label+"\" cannot appear more than once.");
        Macro ans = new Macro(p, isPrivate, this, n, ds, v);
        Macro old = macros.put(n, ans);
        if (old!=null) { macros.put(n, old); throw new ErrorSyntax(p, "You cannot declare more than one macro with the same name \""+n+"\" in the same file."); }
     }
        
    //============================================================================================================================//
    
    /** Add a FUN or PRED declaration. */
    void addFunc(Pos p, Pos isPrivate, Pos isVirtual, String n, Expr f, List<Decl> decls, Expr t, Expr v) throws Err {
    	
    	if (decls==null) decls=new ArrayList<Decl>(); else decls=new ArrayList<Decl>(decls);
        
    	//
    	// The parameter 'f' is a signature reference preceding the function (f.function[])
    	// originally the expression would be added to the declaration list with the name 'this'.
    	// Now it is passed to ast.Func to able to exactly recreate the function. 
    	//
        // if (f!=null) decls.add(0, new Decl(null, null, null, Util.asList(ExprVar.make(f.span(), "this")), f));
    	//
    	
    	// In case we have a virtual function that does not use the 'receiver' 
    	// syntax, use the first parameter as the receiver class and remove it 
		// from the parameter list
    	if(isVirtual != null && f == null) {
    		if (decls.size() < 1) {
    			throw new ErrorSyntax(p, "virtual fun/pred \""+ n +"\" does not declare receiver class");
    		}
    		Decl decl = decls.remove(0);
    		f = decl.expr;
    		
    		//
    		// If the declaration refers to more than one variable, recreate it
    		// removing the first variable name.
    		//
    		if (decl.names.size() != 1) {
    			ConstList<ExprVar> names = decl.names.subList(1, decl.names.size());
    			Decl newDecl = new Decl(decl.isPrivate, decl.disjoint, decl.disjoint2, names, decl.expr);
    			decls.add(0, newDecl);
    		}
    	}
    	
        // Create the function AST node
        Func fn = new Func(p, isPrivate, isVirtual, n, f, decls, t, v);
        
        // Add to the module function list
        SafeList<Func> list = functions.get(n);
        if (list==null) { 
        	list = new SafeList<Func>(); 
        	functions.put(n, list); 
        }
        list.add(fn);
    }
    
    /** Return an unmodifiable list of all functions in this module. */
    public SafeList<Func> getAllFunc() {
        SafeList<Func> ans = new SafeList<Func>();
        for(Map.Entry<String,SafeList<Func>> e: resolvedFunctions.entrySet()) 
        	for(Func func:e.getValue()) 
        		ans.add(func);
        return ans.dup();
    }

    
    /** Resolve virtual dispatcher and 'super' method calls in virtual methods */
	public void resolveVirtualFunctions () throws Err {
	
		// map 'virtual fun/pred name' -> 'root class name' -> 'virtual fun/pred'
		Map<String,Map<String,SafeList<Func>>> dispatchFunctions = new LinkedHashMap<String,Map<String,SafeList<Func>>>();
		
		// Get all the real class hierarchies in the model
		Vector<ModelClassHierarchy> classH = classHierarchy.split(valloyRootObjectName);
		
		// Fill 'resolvedFunctions'.  If not virtual just copy.  If virtual, save the function
		// to generate the dispatcher and translate to Alloy code
		for(Map.Entry<String,SafeList<Func>> e: functions.entrySet()) {
        	
			// map 'root class name' -> 'virtual fun/pred'
        	Map<String,SafeList<Func>> rootToFnMap = new LinkedHashMap<String,SafeList<Func>>();
        	SafeList<Func> resolvedList = new SafeList<Func>(e.getValue().size());
        	
        	for (Func f: e.getValue()) {
        		
        		if(f.isVirtual != null) {
        			
        			// Get the 'this' class name
        			ExprVar thisClass = (ExprVar)f.sigRef;
        			ExprVar rootClass = null;
        			ExprVar superClass = null;
        			
        			// Find the hierarchy of 'this'
        			for(ModelClassHierarchy h: classH) {
        				if (h.contains(thisClass.label)) {
        					rootClass = ExprVar.make(Pos.UNKNOWN, h.getRoot().getName());
        					
        					// If 'this' is not the root, find the parent
        					if (!thisClass.label.equals(rootClass.label)) {
        						superClass = ExprVar.make(Pos.UNKNOWN, h.get(thisClass.label).getParent().getName());
        					}        			        
        				}
        			} 			
        			
        			// check if we found the hierarchy for 'this' class
        			if (rootClass == null){
        				throw new ErrorType(f.pos, "class \"" + thisClass.label + "\" used as receiver for virtual fun/pred \"" + f.label + "\" does not belong to any class hierarchy");
        			}
        			
        			
        			//
        			// Translate the function to Alloy:
        			// - change 'this' to the root class of the hierarchy
        			// - add the original 'this' class name to the fun/pred name
        			//
        			final String name = thisClass + "_" + f.label;
        			Func fn = new Func(f.pos, f.isPrivate, null, name, rootClass, f.params, f.returnDecl, f.body.resolveSuperCall(thisClass, superClass));
        			
					//
			        // Find the list of functions associated with this root
					//
			        SafeList<Func> list = rootToFnMap.get(rootClass.label);
			        if (list==null) { 
			        	list = new SafeList<Func>(); 
			        	rootToFnMap.put(rootClass.label, list); 
			        }
			        list.add(f);
			        
			        // add the translated function to the list
			        f = fn;
        		}
        		
        		resolvedList.add(f);
        	}
        	
        	
        	dispatchFunctions.put(e.getKey(), rootToFnMap);
        	resolvedFunctions.put(e.getKey(), resolvedList);
        }
        
        //
        //
        //
        for(Entry<String, Map<String, SafeList<Func>>> e: dispatchFunctions.entrySet()) {
        	
        	final String dispatchName = e.getKey();
        	SafeList<Func> dispatchList = new SafeList<Func>();
        	
        	for(Entry<String, SafeList<Func>> rootToFnMap: e.getValue().entrySet()) {
        	
        		Expr rootClass = ExprVar.make(Pos.UNKNOWN, rootToFnMap.getKey());
        		
        		// Group functions with the same root class and argument types
        		Map<String , SafeList<Func>> declMap = new LinkedHashMap<String, SafeList<Func>>();
        		
        		for(Func fn: rootToFnMap.getValue()) {	
			        SafeList<Func> list = declMap.get(fn.declTypes);
			        if (list==null) { 
			        	list = new SafeList<Func>(); 
			        	declMap.put(fn.declTypes, list); 
			        }
			        list.add(fn);
        		}
        		
        		
        		for(Entry<String, SafeList<Func>> declMapItem: declMap.entrySet()) {
        			SafeList<Func> functionList = declMapItem.getValue();
        			
        			//
        			// All functions in this list have the same parameter types
        			// Use the first one to get the virtual dispatch parameters
        			//
        			final ConstList<Decl> params = functionList.get(0).params;
        			final Expr returnDecl = functionList.get(0).returnDecl;

        			// get all variable names from the declaration.  The resulting
        			// ExprList expression is [a,b,c,...]
        			List<Expr> paramList = new ArrayList<Expr>();
        			for(Decl d: params){
        				for(ExprVar n: d.names){
        					paramList.add(n);
        				}
        			}
        			final Expr callParams = ExprList.makeJOIN(Pos.UNKNOWN, Pos.UNKNOWN, paramList);

        			// Expr => this.class
        			final Expr checkClass = ExprBadJoin.make(Pos.UNKNOWN, Pos.UNKNOWN, 
        					ExprVar.make(Pos.UNKNOWN, "this"), 
        					ExprVar.make(Pos.UNKNOWN, "class"));

        			Expr dispatchBody = null;

        			for(Func fn: functionList){

        				final Expr className = ExprVar.make(Pos.UNKNOWN, fn.sigRef.toString() + "_VAlloyClassName");
        				final Expr cond = ExprBinary.Op.EQUALS.make(null, null, checkClass, className);

        				final Expr left = 
        					ExprBadJoin.make(Pos.UNKNOWN, Pos.UNKNOWN, 
        							callParams,
        							ExprBadJoin.make(Pos.UNKNOWN, Pos.UNKNOWN, 
        									ExprVar.make(Pos.UNKNOWN, "this"), 
        									ExprVar.make(Pos.UNKNOWN, fn.sigRef.toString() + "_" + fn.label)));


        				dispatchBody = ExprITE.make(Pos.UNKNOWN, cond, left, dispatchBody);
        			}

        			Func f = new Func(Pos.UNKNOWN, Pos.UNKNOWN, null, dispatchName, rootClass, params, returnDecl, dispatchBody);
        			dispatchList.add(f);

        		}
        	}
        	
        	//
        	// Attach dispatch functions
        	//
	        SafeList<Func> list = resolvedFunctions.get(dispatchName);
	        if (list==null) { 
	        	list = new SafeList<Func>(); 
	        	resolvedFunctions.put(dispatchName, list); 
	        }
	        for(Func f: dispatchList)
	        	list.add(f);
	        
        }      
	}
	
    //============================================================================================================================//

    /** Add an ASSERT declaration. */
    String addAssertion(Pos pos, String name, Expr value) throws Err {
        status=3;
        if (name==null || name.length()==0) name="assert$"+(1+asserts.size());
        dup(pos, name, false);
        
        if (asserts.containsKey(name)) {
        	throw new ErrorSyntax(pos, "\""+name+"\" is already the name of an assertion in this module.");
        }
        
        //
        // Special case for empty asserts.  The parser will pass a constant TRUE
        // if the assert body is empty.  Use null to indicate empty body
        //
        if (value instanceof ExprConstant) {
        	ExprConstant c = (ExprConstant)value;
        	if (c.op == ExprConstant.Op.TRUE) {
        		asserts.put(name, null);
        		return name;
        	}
        }
        
        //
        // body is not empty
        //
        asserts.put(name, ExprUnary.Op.NOOP.make(value.span().merge(pos), value));
        return name;
    }
    
    /** Return an unmodifiable list of all assertions in this module. */
    public ConstList<Pair<String,Expr>> getAllAssertions() {
        TempList<Pair<String,Expr>> ans = new TempList<Pair<String,Expr>>(asserts.size());
        for(Map.Entry<String,Expr> e:asserts.entrySet()) {
            Expr x=e.getValue();
            if (x instanceof ExprVar) ans.add(new Pair<String,Expr>(e.getKey(), ((ExprVar)x).expr));
        }
        return ans.makeConst();
    }

    //============================================================================================================================//

    /** Add a FACT declaration. */
    void addFact(Pos pos, String name, Expr value) throws Err {
        status=3;
        if (name==null || name.length()==0) name="fact$"+(1+facts.size());
  
        //
        // Special case for empty facts.  The parser will pass a constant TRUE
        // if the fact body is empty.  Use null to indicate empty body
        //
        if (value instanceof ExprConstant) {
        	ExprConstant c = (ExprConstant)value;
        	if (c.op == ExprConstant.Op.TRUE) {
        		facts.add(new Pair<String,Expr>(name, null)); 
        		return;
        	}
        }
        
        //
        // body is not empty
        //
        facts.add(new Pair<String,Expr>(name, ExprUnary.Op.NOOP.make(value.span().merge(pos), value)));   
    }

  
    /** Return an unmodifiable list of all facts in this module. */
    public SafeList<Pair<String,Expr>> getAllFacts() {
        return (new SafeList<Pair<String,Expr>>(facts)).dup();
    }


    //============================================================================================================================//

    /** Add a COMMAND declaration. */
    void addCommand(boolean followUp, Pos p, String n, boolean c, int o, int b, int seq, int exp, List<CommandScope> s, ExprVar label) throws Err {
    	if (label!=null) p=Pos.UNKNOWN.merge(p).merge(label.pos);
        status=3;
        String labelName = (label != null) ? label.label : null; 
        Command parent = followUp ? commands.get(commands.size()-1) : null;
        Command newcommand = new Command(p, labelName, c, o, b, seq, exp, s, null, ExprVar.make(null, n), parent);
        if (parent!=null) commands.set(commands.size()-1, newcommand); else commands.add(newcommand);
    }

    /** Add a COMMAND declaration. */
    void addCommand(boolean followUp, Pos p, Expr e, boolean c, int o, int b, int seq, int exp, List<CommandScope> s, ExprVar label) throws Err {
    	if (label!=null) p=Pos.UNKNOWN.merge(p).merge(label.pos);
        status=3;
        String labelName = (label != null) ? label.label : null; 
        Command parent = followUp ? commands.get(commands.size()-1) : null;
        Command newcommand = new Command(e.span().merge(p), labelName, c, o, b, seq, exp, s, null, e, parent);
        if (parent!=null) commands.set(commands.size()-1, newcommand); else commands.add(newcommand);
    }

   
    /** Return an unmodifiable list of all commands in this module. */
    public ConstList<Command> getAllCommands() { return ConstList.make(commands); }

    //============================================================================================================================//
    
    Writer write(Writer out) throws IOException{
		
		out.write(this.toString());
		out.write("\n");
		
		for (Open o: this.getOpens()){
			out.write(o.toString() + "\n");
		}
		out.write("\n");
		for (ModelClassHierarchy hierarchy: modelHierarchies){
			if (hierarchy.size()>1){
				out.write(hierarchy.toString());
				out.write("\n");
			}
		}
		
		for (Sig s: this.getAllSigs()) {
			out.write(s.toString() + "\n\n");
		}
		
		for (Func f: this.getAllFunc()) {
			out.write(f.toString() + "\n\n");
		}
		
		
	    for (Map.Entry<String, Expr> a: asserts.entrySet()) {
	    	out.write("assert ");
	    	if (!a.getKey().contains("$"))
	    		out.write(a.getKey() + " ");
	    	
	    	out.write("{\n");	
	    	if (a.getValue() != null) {
	    		StringBuilder sb=new StringBuilder(); 
	    		a.getValue().toString(sb, 2, true);
	    		out.write(sb.toString() + "\n");
	    	}
	    	out.write("}\n\n");
	    }
	    
	    for (Pair<String, Expr> f: facts){
	    	out.write("fact ");
	    	if (!f.a.contains("$"))
	    		out.write(f.a + " ");
	    	
	    	out.write("{\n");	
	    	if (f.b != null) {
	    		StringBuilder sb=new StringBuilder(); 
	    		f.b.toString(sb, 2, true);
	    		out.write(sb.toString() + "\n");
	    	}
	    	out.write("}\n\n");
	    }

		for (Command c: this.getAllCommands()) {
			out.write(c.toString() + "\n\n");
		}
		
    	out.flush();
    	return out;
    }
}
